A:Type, eq:EqDecider(A), B:(AType), f:a:A fp B(a), x:A, v:B(x).
f || x : v  x  dom(f)  f(x) = v 

latex

Definitions	t  T, Top, P  Q, P  Q, x:A. B(x), P & Q, P  Q, x(s), f(x), b, f || g, EqDecider(T), x. t(x), a:A fp B(a), x : v, x  dom(f)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-compatible wf, fpf-single wf, fpf wf, deq wf, fpf-single-dom